\begin{tabbing}
$\forall$\=${\it sv}$:(Id$\rightarrow$($T$:Type $\times$ ($T$ + ($\mathbb{Q}\rightarrow$$T$)))), ${\it av}$:(Knd$\rightarrow$Type), ${\it dis}$:(Id$\rightarrow$Id$\rightarrow\mathbb{B}$),\+
\\[0ex]${\it cl}$:(Id$\rightarrow$($n$:$\mathbb{Z}$ $\times$ base{-}domain{-}type($n$))$\rightarrow$Realizer), ${\it fr}$, ${\it rfr}$:(Id$\rightarrow$Id$\rightarrow$(Knd List)),
\\[0ex]${\it sfr}$:(IdLnk$\rightarrow$Id$\rightarrow$(Knd List)), ${\it afr}$:(Id$\rightarrow$Knd$\rightarrow$((Id List) + Top)),
\\[0ex]${\it bfr}$:(Id$\rightarrow$Knd$\rightarrow$((IdLnk List) + Top)).
\-\\[0ex]($\forall$$k$:Knd. ${\it av}$($k$))
\\[0ex]$\Rightarrow$ \=($\forall$$R$:Realizer.\+
\\[0ex]R{-}FeasibleWitness\{i:l\}($R$; ${\it sv}$; ${\it av}$; ${\it dis}$; ${\it cl}$; ${\it fr}$; ${\it sfr}$; ${\it rfr}$; ${\it afr}$; ${\it bfr}$) $\Rightarrow$ R{-}Feasible($R$))
\-
\end{tabbing}